Given a cardinal $\kappa$, $\kappa$-complete lattices are lattices that have joins and meets of less than $\kappa$ elements (in particular they are bounded). In what follows we shall restrict to the case in which $\kappa$ is inaccessible. In this case the usual distributive lattices have a corresponding $\kappa$-distributive analogue that I considered in my thesis, in which we have a special distributivity property. We say that a lattice is $\kappa$-distributive if, 1) $a \wedge \bigvee_{i<\gamma}b_i=\bigvee_{i<\gamma}a \wedge b_i$ (for $\gamma<\kappa$, which holds whenever the lattice is a Heyting algebra), and 2) if for every $\gamma<\kappa$ and all elements $\{a_f: f \in \gamma^{\beta}, \beta<\gamma\}$ such that
$$a_{f} \leq \bigvee_{g \in \gamma^{\beta+1}, g|_{\beta}=f} a_{g}$$ for all $f \in \gamma^{\beta}, \beta<\gamma$, and
$$a_{f} = \bigwedge_{\alpha<\beta}a_{f|_{\alpha}}$$ for all limit $\beta$, $f \in \gamma^{\beta}, \beta<\gamma$, we have that
$$a_{\emptyset} \leq \bigvee_{f \in \gamma^{\gamma}} \bigwedge_{\beta<\gamma}a_{f|_{\beta}}.$$
In words, condition 2) says that if for each $\gamma<\kappa$ we have in the lattice a tree of type $\gamma^\gamma$ (whose partial order is the reverse order of the lattice) in which every element is below the join of its immediate successors and where at limits levels every element is the meet of its predecessors, then the root element is below the join over all cofinal branches of the elements that are intersections of elements in each cofinal branch of the tree.
$\kappa$-distributivity implies the distributivity property:
$$\bigwedge_{i<\gamma}\bigvee_{j<\gamma}a_{ij} = \bigvee_{f \in \gamma^{\gamma}}\bigwedge_{i<\gamma} a_{if(i)} \qquad (1)$$
and in fact one can see that in a $\kappa$-complete Boolean algebra they are equivalent properties. However $\kappa$-distributivity is stronger in general; for example the interval $[0,1]$ satisfies (1) but is not $\kappa$-distributive.
A $\kappa$-complete filter in the lattice is a filter such that whenever $a_i \in \mathcal{F}$ for every $i \in I$, $|I|<\kappa$, then $\bigwedge_{i \in I}a_i \in \mathcal{F}$. A $\kappa$-prime filter in the lattice is a filter $\mathcal{F}$ such that whenever $\bigvee_{i \in I}a_i$ is in $\mathcal{F}$ for $|I|<\kappa$ then $a_i \in \mathcal{F}$ for some $i \in I$.
I had proven that $\kappa$ is weakly (resp. strongly) compact if and only if every $\kappa$-complete, $\kappa$-distributive lattice of cardinality at most $\kappa$ (resp. of arbitrary cardinality) has a $\kappa$-complete, $\kappa$-prime filter.
What I'm interested in is in a property that I deduced using the weak compactness of $\kappa$. Namely, if we consider the free $\kappa$-complete, $\kappa$-distributive Heyting algebra, the top element 1 happens to be $\kappa$-irreducible, in the sense that whenever we have $1=\bigvee_{i<\gamma} a_i$ for some $\gamma<\kappa$, then $a_i=1$ for some $i$. This is basically an infinitary version of the disjunction property for a certain infinitary intuitionistic logic.
But what I would like to know is if this property per se is a weaker large cardinal assumption in case the free Heyting algebra has two or more generators (in which case the algebra has cardinality $\kappa$). At first sight it seems that the notion of weakly compact cardinal is perhaps too strong to characterize cardinals with such property, and yet the property looks like some form of compactness (it's saying, in fact, that in the free Heyting algebra $\{1\}$ is a $\kappa$-prime filter). So here are my questions:
If $\kappa$ is an inaccessible cardinal such that in the free $\kappa$-complete, $\kappa$-distributive Heyting algebra on at least two generators $1$ is a $\kappa$-irreducible element, can we conclude that $\kappa$ is weakly compact?
I suspect that the answer is no, and in that case I would like to know exactly which type of large cardinal assumption characterizes such property. Is it a new notion? How does it fit into the large cardinal hierarchy? So far we know that it lies between inaccessibility and weak compactness. What is its exact strength?
